b:. ((b))  (b = ff) 

latex

Definitions	left + right, True, tt, Unit, b, P  Q, P  Q, P  Q, x:A. B(x), void, A, P  Q, x:AB(x), False, prop{i:l}, s = t, , t  T, ff, if b then t else f fi , #$n,
Lemmas	ifthenelse wf, bfalse wf, bool wf, false wf, not wf, btrue wf, true wf